#include "Model.hh"

#include <fstream>
#include <sstream>

int Model::get_problem_variable_index(const std::string& var) const
{
  t_var_map::const_iterator it = problem_variables.find(var);

  if (it == problem_variables.end())
    return -1;
  else
    return it->second;
}

int Model::parse_size(std::istream& in)
{
  int nb_states;

  in >> nb_states;

  return nb_states;
}

void Model::parse_model(std::istream& in)
{
  successor_relation	= bddfalse;
  label_relation	= bddfalse;

  nb_problem_variables = 0;

  while (!in.eof())
    {
      parse_state(in);

      // skip whitespaces or empty lines
      while (in.peek() == ' '
	     || in.peek() == '\n')
	{
	  in.ignore();
	}
    }
}

//privates

void Model::parse_state(std::istream& in)
{
  int state_number;

  in >> state_number;

  bdd state = make_state(state_number);

  //std::clog << "state = " << state << std::endl;

  bdd variables = parse_variables(in);

  label_relation |= state & variables;  

  //std::clog << "label_relation = " << label_relation << std::endl;
  
  bdd successors = parse_successors(in);

  successor_relation |= state & successors;

  //std::clog << "successor_relation = " << successor_relation << std::endl;
}

bdd Model::parse_variables(std::istream& in)
{
  std::istringstream variables;
  {
    std::string buffer;
    getline(in, buffer);
    variables.str(buffer);
  }

  bdd bdd_variable = bddtrue;

  while (!variables.eof())
    {
      std::string variable;
      variables >> variable;

      bool is_not = (variable[0] == '!');
      
      if (is_not)
	variable.erase(0, 1); // erase the '!' char

      int problem_variable_index;
      t_var_map::iterator it = problem_variables.find(variable);
      
      if (it == problem_variables.end())
	{
	  int new_index = nb_state_variables * 2 + nb_problem_variables;

	  problem_variables[variable] = new_index;
	  problem_variable_index = new_index;

	  ++nb_problem_variables;

	  bdd_extvarnum(1);
	}
      else
	{
	  problem_variable_index = it->second;
	}

      if (is_not)
	bdd_variable &= bdd_nithvar(problem_variable_index);
      else
	bdd_variable &= bdd_ithvar(problem_variable_index);
    }

  return bdd_variable;
}

bdd Model::parse_successors(std::istream& in)
{
  std::istringstream successors;
  {
    std::string buffer;
    getline(in, buffer);
    successors.str(buffer);
  }

  bdd successor_relations = bddfalse;

  while (!successors.eof())
    {
      int successor;
      successors >> successor;

      bdd bdd_successor = make_state(successor);

      successor_relations |= reverse_state(bdd_successor);
    }

  return successor_relations;
}

bdd Model::make_state(int state_number) const
{
  bdd state = bddtrue;

  for (int i = 0; i < nb_state_variables; ++i)
    {
      if ((1 << i) & state_number)
	{
	  state &= bdd_ithvar(i);
	}
      else
	{
	  state &= bdd_nithvar(i);
	}
    }

  return state;
}

bdd Model::reverse_state(bdd state) const
{
  for (int i = 0; i < nb_state_variables; ++i)
    {
      bddPair* pair = bdd_newpair();

      int reverse_variable = i + nb_state_variables;

      bdd_setpair(pair, i, reverse_variable);

      state = bdd_replace(state, pair);

      bdd_freepair(pair);
    }

  return state;
}

bdd Model::unreverse_state(bdd state) const
{
  for (int i = nb_state_variables; i < 2 * nb_state_variables; ++i)
    {
      bddPair* pair = bdd_newpair();

      int reverse_variable = i - nb_state_variables;

      bdd_setpair(pair, i, reverse_variable);

      state = bdd_replace(state, pair);

      bdd_freepair(pair);
    }

  return state;
}

// public static
int Model::compute_nb_variables(int nb_nodes)
{
  int nb_variables = 0;
  --nb_nodes;

  while (nb_nodes > 0)
    {
      nb_nodes = nb_nodes >> 1;

      ++nb_variables;
    }

  return nb_variables;
}

bdd Model::get_state_high() const
{
  return make_state((1 << nb_state_variables) - 1);
}

bdd Model::get_problem_variables() const
{
  bdd variables = bddtrue;

  for (t_var_map::const_iterator it = problem_variables.begin();
       it != problem_variables.end(); ++it)
    {
      variables &= bdd_ithvar(it->second);
    }

  return variables;
}
